es:ES, L:(Id List).
fischer(L)
 (e:E, j:Id.
 Newround(e)
  (j  L)
  ((j = loc(e)))
  (e':E.
  (isrcv(e'))
   (sender(e') = e)
   (loc(e') = j)
   (tag(e') = "free"  Id)
   (lnk(e') = <loc(e), j, "z">  IdLnk)
   the rcv(free message from e to j) loc e' )) 

latex

Definitions	t  T, "$x", Id, <a, b>, x:A. B(x), loc(e), IdLnk, x:A  B(x), ES, type List, fischer(L), t.1, E, Atom$n, P & Q, Newround(e), x:A. B(x), (x  l), P  Q, A, if b then t else f fi , b, s = t, (e sends on l with tag tg), the rcv(free message from e1 to j), , isrcv(e), sender(e), tag(e), lnk(e), e loc e' , xL. P(x), P  Q, P  Q, P  Q, False, x:AB(x), A c B, left + right
Lemmas	assert-eq-id, IdLnk wf, es-lnk wf, es-tag wf, es-sender wf, assert wf, es-isrcv wf, not wf, l member wf, f-newround wf, es-E wf, fischer wf, Id wf, event system wf, es-first-from-is-first, es-loc wf